| CONSTR_PROPERTIES_com |
9,38 |
|
Predicates for constructive properties of propositions, and
lemmas characterizing how these predicates are inherited.
Worthwhile sometime redoing thms for soft abstractions
in terms of the underlying hard abstractions / primitives.
